T:Type, L:(T List). ((null(L)))  (L':T List. (L = append(L'; cons(last(L); [])))) 

latex

Definitions	t  T, P  Q, x:A. B(x), prop{i:l}, gt(i; j), x:A. B(x), False, A  B, P  Q, int_iseg(i; j), P  Q, P  Q, A, l[i], last(L), True, T, ge(i; j), , Y, tl(l), ||as||
Lemmas	null wf, assert wf, not wf, non nil length, assert of null, not functionality wrt iff, last wf, append wf, length wf1, firstn wf, nth tl wf, list decomp, le wf, length nth tl, hd wf, true wf, squash wf, ge wf, non neg length, nat wf, length zero, append firstn lastn